es:ES, Out, Sys:AbsInterface(Top), Ack:AbsInterface(), g:sys-antecedent(es;Ack),
chain:({e:E| ((e  Sys))  ((e  Ack))} (Id List)).
(E(Out) r E(Sys))
 chain-config(es;p-conditional(Ack; Sys);chain)
 (e:E(Sys). ((e  Out))  (loc(e) = last(chain(e))  Id))
 (e:E(Ack).
 ((loc(g(e)) = loc(e)  Id))
  (adjacent(Id;chain(e);loc(e);loc(g(e))) & adjacent(Id;chain(g(e));loc(e);loc(g(e)))))
 (e:E(Ack). (loc(g(e)) = loc(e)  Id)  ((e  Out)))
 chain-consistent(g;e.rev(chain(e))) 

latex

Up	abstract chain replication
Definitions	t  T, , AbsInterface(A), Top, sys-antecedent(es;Sys), x:AB(x), s = t, ES, type List, x:A  B(x), b, left + right, {x:A| B(x)} , e  X, P  Q, E, E(X), !Void(), x:A.B(x), P  Q, x:A. B(x), P  Q, P & Q, P  Q, f(x)?z, strong-subtype(A;B), a:A fp B(a), let x,y = A in B(x;y), t.1, chain-config(es;Sys;chain), [car / cdr], <a, b>, x:A. B(x), a < b, A, L1  L2, no_repeats(T;l), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Atom$n, p-conditional(f; g), , Type, , , Outcome, #$n, A  B, ||as||, False, l[i], |g|, S  T, A c B, [], True, increasing(f;k), (e <loc e'), Unit, ff, inr x , tt, inl x , T, Dec(P), b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), y is f*(x), r  s, r < s, q-rel(r;x), l_disjoint(T;l1;l2), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P), f  g, EState(T), , EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'), x,y. t(x;y), suptype(S; T), first(e), pred(e), x.A(x), x. t(x), {T}, last(L), adjacent(T;L;x;y), -n, n+m, n - m, i  j < k, {i..j}, chain-consistent(f;chain), rev(as), a = b, x  dom(f), es-empty-interface, Id, f(a), loc(e), (x  l), f o g, isempty{isempty_compseq_tag_def:ObjectId}(e), hd(l), source(l), destination(l), es-init(es;e), isrcv(e), kind(e), es-first-from(es;e;l;tg), isrcv(k), lastchange(x;e), (last change to x before e), s ~ t
Lemmas	adjacent-reverse, hd-reverse, es-isrcv-loc, es-loc-pred, es-locl-iff, es-E-interface-conditional-subtype1, chain-config-reverse, not functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, assert-eq-id, iff wf, rev implies wf, eq id wf, es-le wf, chain-consistent wf, int seg wf, adjacent wf, es-E-interface-subtype rel, last wf, no repeats wf, es-locl wf, sublist wf, chain-config wf, subtype rel function, p-conditional wf, es-E-interface-conditional2, es-causle wf, sys-antecedent wf, le wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, val-axiom wf, cless wf, qle wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, event system wf, sq stable from decidable, decidable assert, btrue wf, bfalse wf, unit wf, bool wf, es-E-interface-conditional-subtype2, assert wf, es-is-interface wf, true wf, nil member, length wf2, not wf, false wf, length wf1, select wf, Id wf, l member wf, es-loc wf, es-E wf, es-E-interface wf, es-interface-conditional, member wf, es-interface wf, es-interface-subtype rel, top wf, nat wf, subtype rel wf